g:OGrp. *  |g||g||g| 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OCMon, OGrp, |g|
Definitions	t  T, x:A. B(x), |g|, Mon, AbMon, OCMon, OGrp, , x f y, P  Q
Lemmas	ocgrp wf, hgrp car wf, grp op wf, grp id wf, grp leq wf, hgrp car properties, grp op polarity